(set-info :source |fuzzsmt|)
(set-info :smt-lib-version 2.0)
(set-info :category "random")
(set-info :status unknown)
(set-logic QF_NRA)
(declare-fun v0 () Real)
(declare-fun v1 () Real)
(assert (let ((e2 1))
(let ((e3 3))
(let ((e4 (+ v1 v0)))
(let ((e5 (+ v1 v0)))
(let ((e6 (* e5 v1)))
(let ((e7 (+ e6 v1)))
(let ((e8 (+ e6 e4)))
(let ((e9 (- e7 e8)))
(let ((e10 (- v0 e8)))
(let ((e11 (- e9 e5)))
(let ((e12 (* e6 v0)))
(let ((e13 (- e5 e12)))
(let ((e14 (+ e13 e12)))
(let ((e15 (* e12 e7)))
(let ((e16 (/ e3 (- e2))))
(let ((e17 (< e5 v0)))
(let ((e18 (<= v0 e7)))
(let ((e19 (distinct e12 e16)))
(let ((e20 (> e11 v1)))
(let ((e21 (>= e11 e11)))
(let ((e22 (= e5 e16)))
(let ((e23 (= v1 v1)))
(let ((e24 (>= e8 e11)))
(let ((e25 (> e15 e9)))
(let ((e26 (>= e10 v0)))
(let ((e27 (= e4 e11)))
(let ((e28 (= e15 v0)))
(let ((e29 (> e16 e15)))
(let ((e30 (>= e6 v0)))
(let ((e31 (<= e9 v1)))
(let ((e32 (< e8 v0)))
(let ((e33 (<= e16 e16)))
(let ((e34 (= v1 e11)))
(let ((e35 (distinct e12 v0)))
(let ((e36 (< e8 e10)))
(let ((e37 (distinct e6 e7)))
(let ((e38 (= e4 e6)))
(let ((e39 (> e15 e9)))
(let ((e40 (= e14 e12)))
(let ((e41 (< e7 e8)))
(let ((e42 (= e14 e4)))
(let ((e43 (distinct v0 e12)))
(let ((e44 (<= e10 e15)))
(let ((e45 (>= v0 e12)))
(let ((e46 (> e9 e11)))
(let ((e47 (<= e9 e14)))
(let ((e48 (<= e7 e14)))
(let ((e49 (< e14 e7)))
(let ((e50 (<= e6 e14)))
(let ((e51 (distinct e4 e11)))
(let ((e52 (distinct e14 e7)))
(let ((e53 (distinct e9 e5)))
(let ((e54 (> e15 e14)))
(let ((e55 (= e15 e12)))
(let ((e56 (>= v1 e4)))
(let ((e57 (> e5 e8)))
(let ((e58 (> e9 e6)))
(let ((e59 (< e9 e15)))
(let ((e60 (<= e16 e10)))
(let ((e61 (>= e14 e16)))
(let ((e62 (distinct e10 e14)))
(let ((e63 (< e7 e4)))
(let ((e64 (= e7 e6)))
(let ((e65 (<= e7 v1)))
(let ((e66 (< e6 e15)))
(let ((e67 (> e15 e16)))
(let ((e68 (<= e6 e11)))
(let ((e69 (< e10 e15)))
(let ((e70 (distinct v0 e8)))
(let ((e71 (< e6 e5)))
(let ((e72 (> e5 e12)))
(let ((e73 (>= e15 e8)))
(let ((e74 (< e9 e15)))
(let ((e75 (<= e16 e14)))
(let ((e76 (>= e15 e15)))
(let ((e77 (<= e11 v0)))
(let ((e78 (= e12 e8)))
(let ((e79 (>= e4 v1)))
(let ((e80 (<= e7 e15)))
(let ((e81 (= e15 e5)))
(let ((e82 (< e14 e6)))
(let ((e83 (> e11 e5)))
(let ((e84 (distinct e16 e5)))
(let ((e85 (= e8 e12)))
(let ((e86 (= e4 e5)))
(let ((e87 (> e13 e4)))
(let ((e88 (> e5 e6)))
(let ((e89 (<= v0 v0)))
(let ((e90 (< v0 e13)))
(let ((e91 (>= e13 e7)))
(let ((e92 (>= e5 e6)))
(let ((e93 (distinct v0 e9)))
(let ((e94 (>= e12 e5)))
(let ((e95 (> e5 e4)))
(let ((e96 (= e11 e14)))
(let ((e97 (> e15 e12)))
(let ((e98 (= e4 e12)))
(let ((e99 (>= e6 e13)))
(let ((e100 (<= e13 v0)))
(let ((e101 (>= e14 e15)))
(let ((e102 (= e7 e8)))
(let ((e103 (= e16 e4)))
(let ((e104 (= e11 e16)))
(let ((e105 (> e9 v1)))
(let ((e106 (<= e11 e12)))
(let ((e107 (> e14 e11)))
(let ((e108 (distinct e14 e8)))
(let ((e109 (<= e12 e15)))
(let ((e110 (> v1 e6)))
(let ((e111 (> e10 e15)))
(let ((e112 (=> e39 e57)))
(let ((e113 (=> e70 e48)))
(let ((e114 (= e51 e35)))
(let ((e115 (= e55 e33)))
(let ((e116 (or e58 e54)))
(let ((e117 (not e97)))
(let ((e118 (=> e88 e46)))
(let ((e119 (or e40 e40)))
(let ((e120 (or e81 e76)))
(let ((e121 (= e73 e45)))
(let ((e122 (xor e63 e26)))
(let ((e123 (not e56)))
(let ((e124 (= e41 e22)))
(let ((e125 (ite e116 e69 e64)))
(let ((e126 (ite e82 e84 e92)))
(let ((e127 (xor e67 e60)))
(let ((e128 (not e110)))
(let ((e129 (ite e79 e101 e34)))
(let ((e130 (not e119)))
(let ((e131 (xor e109 e20)))
(let ((e132 (ite e115 e42 e71)))
(let ((e133 (not e19)))
(let ((e134 (and e78 e85)))
(let ((e135 (not e120)))
(let ((e136 (= e127 e112)))
(let ((e137 (or e43 e118)))
(let ((e138 (and e27 e68)))
(let ((e139 (or e106 e135)))
(let ((e140 (= e18 e77)))
(let ((e141 (xor e96 e105)))
(let ((e142 (= e124 e59)))
(let ((e143 (or e93 e129)))
(let ((e144 (and e36 e90)))
(let ((e145 (not e130)))
(let ((e146 (=> e24 e53)))
(let ((e147 (not e121)))
(let ((e148 (and e103 e113)))
(let ((e149 (and e89 e147)))
(let ((e150 (or e128 e91)))
(let ((e151 (not e137)))
(let ((e152 (not e83)))
(let ((e153 (not e21)))
(let ((e154 (ite e25 e31 e123)))
(let ((e155 (not e142)))
(let ((e156 (xor e148 e66)))
(let ((e157 (or e65 e125)))
(let ((e158 (and e114 e102)))
(let ((e159 (or e62 e143)))
(let ((e160 (not e99)))
(let ((e161 (not e140)))
(let ((e162 (not e107)))
(let ((e163 (not e52)))
(let ((e164 (or e139 e95)))
(let ((e165 (ite e104 e156 e44)))
(let ((e166 (and e155 e80)))
(let ((e167 (not e32)))
(let ((e168 (and e122 e134)))
(let ((e169 (and e166 e153)))
(let ((e170 (=> e141 e161)))
(let ((e171 (= e23 e28)))
(let ((e172 (ite e100 e98 e163)))
(let ((e173 (and e29 e168)))
(let ((e174 (and e133 e47)))
(let ((e175 (= e154 e154)))
(let ((e176 (ite e87 e175 e160)))
(let ((e177 (ite e164 e158 e171)))
(let ((e178 (ite e150 e170 e172)))
(let ((e179 (= e136 e50)))
(let ((e180 (xor e49 e126)))
(let ((e181 (xor e38 e131)))
(let ((e182 (=> e74 e159)))
(let ((e183 (ite e86 e169 e111)))
(let ((e184 (= e94 e183)))
(let ((e185 (= e176 e157)))
(let ((e186 (=> e181 e144)))
(let ((e187 (ite e37 e146 e72)))
(let ((e188 (= e173 e75)))
(let ((e189 (and e151 e17)))
(let ((e190 (xor e30 e179)))
(let ((e191 (and e108 e108)))
(let ((e192 (ite e180 e165 e182)))
(let ((e193 (or e138 e167)))
(let ((e194 (or e174 e152)))
(let ((e195 (ite e191 e192 e185)))
(let ((e196 (= e117 e149)))
(let ((e197 (xor e145 e132)))
(let ((e198 (ite e186 e186 e190)))
(let ((e199 (= e195 e184)))
(let ((e200 (= e194 e61)))
(let ((e201 (=> e178 e187)))
(let ((e202 (or e193 e198)))
(let ((e203 (xor e162 e177)))
(let ((e204 (xor e200 e188)))
(let ((e205 (=> e203 e202)))
(let ((e206 (not e201)))
(let ((e207 (not e199)))
(let ((e208 (= e204 e189)))
(let ((e209 (not e206)))
(let ((e210 (ite e205 e197 e207)))
(let ((e211 (not e210)))
(let ((e212 (or e208 e196)))
(let ((e213 (xor e211 e209)))
(let ((e214 (or e213 e213)))
(let ((e215 (xor e214 e212)))
e215
)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))

(check-sat)
